basic
\\[0ex]IsAction($A$;$x$;$e$;$S$;$f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$($\forall$$a$:$A$, $b$:$A$, $u$:$S$. (($a$ $x$ $b$) $f$ $u$) = ($a$ $f$ ($b$ $f$ $u$)) $\in$ $S$) \& ($\forall$$u$:$S$. ($e$ $f$ $u$) = $u$ $\in$ $S$)